InforLorV4, Main, Exploration, bibRecord, 003098

Cryptographic Protocols Analysis in Event B

Identifieur interne : 003098 ( Main/Exploration ); précédent : 003097; suivant : 003099

Cryptographic Protocols Analysis in Event B

Auteurs : Nazim Benaissa [France] ; Dominique Méry [France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:692151CE2CA7E5E8A2457CF08C5C2400EFFEAFB2

Abstract

Abstract: We consider the proof-based development of cryptographic protocols satisfying security properties. For instance, the model of Dolev-Yao provides a way to integrate a description of possible attacks, when designing a protocol. We use existing protocols and want to provide a systematic way to prove but also to design cryptographic protocols; moreover, we would like to provide proof-based guidelines or patterns for integrating cryptographic elements in an existing protocol. The goal of the paper is to present a first attempt to mix design patterns (as in software engineering) and formal methods (as a verification tool). We illustrate the technique on the well known Needham-Schroeder public key protocol and Blake-Wilson-Menezes key transport protocol. The underlying modelling language is Event B and is supported by the RODIN platform, which is used to validate models.

Url:

https://api.istex.fr/ark:/67375/HCB-R9RF6TWG-Q/fulltext.pdf

DOI: 10.1007/978-3-642-11486-1_24

Affiliations:

Links toward previous steps (curation, corpus...)

to stream Istex, to step Corpus: 001847
to stream Istex, to step Curation: 001828
to stream Istex, to step Checkpoint: 000860
to stream Main, to step Merge: 003155
to stream Main, to step Curation: 003098

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Cryptographic Protocols Analysis in Event B</title>
<author><name sortKey="Benaissa, Nazim" sort="Benaissa, Nazim" uniqKey="Benaissa N" first="Nazim" last="Benaissa">Nazim Benaissa</name>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:692151CE2CA7E5E8A2457CF08C5C2400EFFEAFB2</idno>
<date when="2010" year="2010">2010</date>
<idno type="doi">10.1007/978-3-642-11486-1_24</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-R9RF6TWG-Q/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001847</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001847</idno>
<idno type="wicri:Area/Istex/Curation">001828</idno>
<idno type="wicri:Area/Istex/Checkpoint">000860</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000860</idno>
<idno type="wicri:doubleKey">0302-9743:2010:Benaissa N:cryptographic:protocols:analysis</idno>
<idno type="wicri:Area/Main/Merge">003155</idno>
<idno type="wicri:Area/Main/Curation">003098</idno>
<idno type="wicri:Area/Main/Exploration">003098</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Cryptographic Protocols Analysis in Event B</title>
<author><name sortKey="Benaissa, Nazim" sort="Benaissa, Nazim" uniqKey="Benaissa N" first="Nazim" last="Benaissa">Nazim Benaissa</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>Université Henri Poincaré Nancy 1 and LORIA, BP 239, 54506, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>Université Henri Poincaré Nancy 1 and LORIA, BP 239, 54506, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We consider the proof-based development of cryptographic protocols satisfying security properties. For instance, the model of Dolev-Yao provides a way to integrate a description of possible attacks, when designing a protocol. We use existing protocols and want to provide a systematic way to prove but also to design cryptographic protocols; moreover, we would like to provide proof-based guidelines or patterns for integrating cryptographic elements in an existing protocol. The goal of the paper is to present a first attempt to mix design patterns (as in software engineering) and formal methods (as a verification tool). We illustrate the technique on the well known Needham-Schroeder public key protocol and Blake-Wilson-Menezes key transport protocol. The underlying modelling language is Event B and is supported by the RODIN platform, which is used to validate models.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Nancy</li>
<li>Vandœuvre-lès-Nancy</li>
</settlement>
<orgName><li>Centre national de la recherche scientifique</li>
<li>Institut national de recherche en informatique et en automatique</li>
<li>Laboratoire lorrain de recherche en informatique et ses applications</li>
<li>Mosel (Loria)</li>
<li>Université de Lorraine</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Benaissa, Nazim" sort="Benaissa, Nazim" uniqKey="Benaissa N" first="Nazim" last="Benaissa">Nazim Benaissa</name>
</region>
<name sortKey="Benaissa, Nazim" sort="Benaissa, Nazim" uniqKey="Benaissa N" first="Nazim" last="Benaissa">Nazim Benaissa</name>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003098 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003098 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:692151CE2CA7E5E8A2457CF08C5C2400EFFEAFB2
   |texte=   Cryptographic Protocols Analysis in Event B
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Cryptographic Protocols Analysis in Event B

Cryptographic Protocols Analysis in Event B

Source :

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri